(set-logic BV)

(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))

(synth-fun f ( (x (BitVec 64))) (BitVec 64)
(

(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
                    (shl1 Start)
 		    (shr1 Start)
		    (shr4 Start)
		    (shr16 Start)
		    (bvand Start Start)
		    (bvor Start Start)
		    (bvxor Start Start)
		    (bvadd Start Start)
		    (if0 Start Start Start)
 ))
)
)
(constraint (= (f #x98095205D52F3184) #xF7FFEFFFAAFDCEFF))
(constraint (= (f #x46129A3EF88EB4C4) #xFBFFF7DD17775FBB))
(constraint (= (f #x5B2F0053B6864522) #xFEDDFFFECDFFBBFD))
(constraint (= (f #x97E0D71886676C21) #xFE9FFAEF7F999BFF))
(constraint (= (f #xF4E8EDE17F156564) #xFBB7733FE8EEBBBB))
(constraint (= (f #x00000000001C6E85) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #x00000000001F2E66) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #x000000000015F247) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #x0000000000165384) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #x00000000001217A7) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #x78F657674F5380ED) #xFF79BA99BBAEFFF3))
(constraint (= (f #xB37D045D45C23468) #xFCCAFFBABBBFDFBF))
(constraint (= (f #xCD114FE6C5E541AE) #xF3EEFB19BBBBBFF5))
(constraint (= (f #x836EBB9626DBBBC9) #xFFD9546FDDB64477))
(constraint (= (f #x35902E91A4E3EA0C) #xFEEFFD7EFFBDD5FF))
(constraint (= (f #x0000000000000002) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #x0000000000000003) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #xE0C21C601442A496) #x00000E0C21C60144))
(constraint (= (f #x528EDB05A7D80214) #x00000528EDB05A7D))
(constraint (= (f #xF010527904F83E76) #x00000F010527904F))
(constraint (= (f #x78736C3BCBD552D4) #x0000078736C3BCBD))
(constraint (= (f #xE3A37EDC9421E517) #x00000E3A37EDC942))
(constraint (= (f #x0000000000101F69) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #x00000000001F45C8) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #x0000000000166828) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #x00000000001384ED) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #x0000000000119FFF) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #x000000000010FCF0) #x0000000000000001))
(constraint (= (f #x00000000001CFFD7) #x0000000000000001))
(constraint (= (f #x000000000017C014) #x0000000000000001))
(constraint (= (f #x00000000001A2CF1) #x0000000000000001))
(constraint (= (f #x0000000000155291) #x0000000000000001))
(constraint (= (f #xAAAAAAAAAAAAAAAB) #x00000AAAAAAAAAAA))
(constraint (= (f #x43F862DC137D9A5B) #x0000043F862DC137))
(constraint (= (f #x51D8F5FF916FBD59) #x0000051D8F5FF916))
(constraint (= (f #xA9276BD7BCE9148F) #x00000A9276BD7BCE))
(constraint (= (f #x5C3C65200A4E0F9B) #x000005C3C65200A4))
(constraint (= (f #x5F1F5F58DB7AAC9E) #x000005F1F5F58DB7))
(constraint (= (f #x00000000001CDD3A) #x0000000000000001))
(constraint (= (f #x00000000001D84BE) #x0000000000000001))
(constraint (= (f #x0000000000157B6F) #x0000000000000001))
(constraint (= (f #x00000000001623AF) #x0000000000000001))
(constraint (= (f #x00000000001308DE) #x0000000000000001))
(check-synth)
